In highly secure computer systems, there is often a need to share information between networks with differing security level. For example, an unclassified network may need to share information with a top-secret network. High-assurance guards are utilized in highly secure computer systems to interconnect networks of differing security level.
However, in order to receive the desired “high-assurance” or “trusted” certification from government organizations such as the National Computer Security Center (NCSC), such guards must be subjected to an evaluation program (such as the Trusted Products Evaluation Program (TPEP)) in which they are tested against a comprehensive set of security-related criteria. Guards that interconnect unclassified and top secret networks need to be accredited to protection level 5 (PL5). Further, such evaluation typically requires construction and solution of complex mathematical proofs designed to prove the “correctness” of the guard being evaluated. Unfortunately, constructing and solving such proofs can make the evaluation process a complex, time-consuming and expensive undertaking.
Therefore, it may be desirable to provide high-assurance routing of information between networks of differing security level which addresses the above-referenced problems and limitations of the current solutions.